(DEFPROP ANDOR 
 (LAMBDA(C UNL EXL PF)
  (PROG (Z1 Z2)
	(SETQ Z1 (CADR C))
	(SETQ Z2 (CADDR C))
	(COND
	 ((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
	  (RETURN (LIST (QUOTE AND) Z1 Z2)))
	 ((EQ (CAR Z1) (QUOTE AND))
	  (RETURN
	   (LIST (QUOTE AND)
		 (CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
		 (CNF1 (LIST (QUOTE OR) (CADDR Z1) (COPY Z2)) UNL EXL T))))
	 ((EQ (CAR Z2) (QUOTE AND))
	  (RETURN
	   (LIST (QUOTE AND)
		 (CNF1 (LIST (QUOTE OR) (CADR Z2) (COPY Z1)) UNL EXL T)
		 (CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
	 (T (RETURN (LIST (QUOTE OR) Z1 Z2)))))) 
EXPR)

(DEFPROP BAKSUB 
 (LAMBDA(L R)
  (PROG (Z U1 U4)
	(SETQ Z L)
   ED4  (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
	(SETQ U1 R)
   ED3  (SETQ U4 (CAR Z))
   ED1  (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
   ED6  (SETQ U1 (CDR U1))
	(COND (U1 (GO ED1)))
   ED6A (SETQ Z (CDR Z))
	(GO ED4)
   ED2  (DEL U4)
	(GO ED4))) 
EXPR)